WORST_CASE(?,O(n^3)) * Step 1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: if'insert(false(),x,y,ys) -> cons(y,insert(x,ys)) if'insert(true(),x,y,ys) -> cons(x,cons(y,ys)) insert(x,cons(y,ys)) -> if'insert(leq(x,y),x,y,ys) insert(x,nil()) -> cons(x,nil()) leq(0(),y) -> true() leq(s(x),0()) -> false() leq(s(x),s(y)) -> leq(x,y) sort(cons(x,xs)) -> insert(x,sort(xs)) sort(nil()) -> nil() - Signature: {if'insert/4,insert/2,leq/2,sort/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {if'insert,insert,leq,sort} and constructors {0,cons,false ,nil,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)) if'insert#(true(),x,y,ys) -> c_2() insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys),leq#(x,y)) insert#(x,nil()) -> c_4() leq#(0(),y) -> c_5() leq#(s(x),0()) -> c_6() leq#(s(x),s(y)) -> c_7(leq#(x,y)) sort#(cons(x,xs)) -> c_8(insert#(x,sort(xs)),sort#(xs)) sort#(nil()) -> c_9() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)) if'insert#(true(),x,y,ys) -> c_2() insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys),leq#(x,y)) insert#(x,nil()) -> c_4() leq#(0(),y) -> c_5() leq#(s(x),0()) -> c_6() leq#(s(x),s(y)) -> c_7(leq#(x,y)) sort#(cons(x,xs)) -> c_8(insert#(x,sort(xs)),sort#(xs)) sort#(nil()) -> c_9() - Weak TRS: if'insert(false(),x,y,ys) -> cons(y,insert(x,ys)) if'insert(true(),x,y,ys) -> cons(x,cons(y,ys)) insert(x,cons(y,ys)) -> if'insert(leq(x,y),x,y,ys) insert(x,nil()) -> cons(x,nil()) leq(0(),y) -> true() leq(s(x),0()) -> false() leq(s(x),s(y)) -> leq(x,y) sort(cons(x,xs)) -> insert(x,sort(xs)) sort(nil()) -> nil() - Signature: {if'insert/4,insert/2,leq/2,sort/1,if'insert#/4,insert#/2,leq#/2,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1 ,true/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/1,c_8/2,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {if'insert#,insert#,leq#,sort#} and constructors {0,cons ,false,nil,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,4,5,6,9} by application of Pre({2,4,5,6,9}) = {1,3,7,8}. Here rules are labelled as follows: 1: if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)) 2: if'insert#(true(),x,y,ys) -> c_2() 3: insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys),leq#(x,y)) 4: insert#(x,nil()) -> c_4() 5: leq#(0(),y) -> c_5() 6: leq#(s(x),0()) -> c_6() 7: leq#(s(x),s(y)) -> c_7(leq#(x,y)) 8: sort#(cons(x,xs)) -> c_8(insert#(x,sort(xs)),sort#(xs)) 9: sort#(nil()) -> c_9() * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)) insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys),leq#(x,y)) leq#(s(x),s(y)) -> c_7(leq#(x,y)) sort#(cons(x,xs)) -> c_8(insert#(x,sort(xs)),sort#(xs)) - Weak DPs: if'insert#(true(),x,y,ys) -> c_2() insert#(x,nil()) -> c_4() leq#(0(),y) -> c_5() leq#(s(x),0()) -> c_6() sort#(nil()) -> c_9() - Weak TRS: if'insert(false(),x,y,ys) -> cons(y,insert(x,ys)) if'insert(true(),x,y,ys) -> cons(x,cons(y,ys)) insert(x,cons(y,ys)) -> if'insert(leq(x,y),x,y,ys) insert(x,nil()) -> cons(x,nil()) leq(0(),y) -> true() leq(s(x),0()) -> false() leq(s(x),s(y)) -> leq(x,y) sort(cons(x,xs)) -> insert(x,sort(xs)) sort(nil()) -> nil() - Signature: {if'insert/4,insert/2,leq/2,sort/1,if'insert#/4,insert#/2,leq#/2,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1 ,true/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/1,c_8/2,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {if'insert#,insert#,leq#,sort#} and constructors {0,cons ,false,nil,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)) -->_1 insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys),leq#(x,y)):2 -->_1 insert#(x,nil()) -> c_4():6 2:S:insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys),leq#(x,y)) -->_2 leq#(s(x),s(y)) -> c_7(leq#(x,y)):3 -->_2 leq#(s(x),0()) -> c_6():8 -->_2 leq#(0(),y) -> c_5():7 -->_1 if'insert#(true(),x,y,ys) -> c_2():5 -->_1 if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)):1 3:S:leq#(s(x),s(y)) -> c_7(leq#(x,y)) -->_1 leq#(s(x),0()) -> c_6():8 -->_1 leq#(0(),y) -> c_5():7 -->_1 leq#(s(x),s(y)) -> c_7(leq#(x,y)):3 4:S:sort#(cons(x,xs)) -> c_8(insert#(x,sort(xs)),sort#(xs)) -->_2 sort#(nil()) -> c_9():9 -->_1 insert#(x,nil()) -> c_4():6 -->_2 sort#(cons(x,xs)) -> c_8(insert#(x,sort(xs)),sort#(xs)):4 -->_1 insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys),leq#(x,y)):2 5:W:if'insert#(true(),x,y,ys) -> c_2() 6:W:insert#(x,nil()) -> c_4() 7:W:leq#(0(),y) -> c_5() 8:W:leq#(s(x),0()) -> c_6() 9:W:sort#(nil()) -> c_9() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 9: sort#(nil()) -> c_9() 6: insert#(x,nil()) -> c_4() 5: if'insert#(true(),x,y,ys) -> c_2() 7: leq#(0(),y) -> c_5() 8: leq#(s(x),0()) -> c_6() * Step 4: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)) insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys),leq#(x,y)) leq#(s(x),s(y)) -> c_7(leq#(x,y)) sort#(cons(x,xs)) -> c_8(insert#(x,sort(xs)),sort#(xs)) - Weak TRS: if'insert(false(),x,y,ys) -> cons(y,insert(x,ys)) if'insert(true(),x,y,ys) -> cons(x,cons(y,ys)) insert(x,cons(y,ys)) -> if'insert(leq(x,y),x,y,ys) insert(x,nil()) -> cons(x,nil()) leq(0(),y) -> true() leq(s(x),0()) -> false() leq(s(x),s(y)) -> leq(x,y) sort(cons(x,xs)) -> insert(x,sort(xs)) sort(nil()) -> nil() - Signature: {if'insert/4,insert/2,leq/2,sort/1,if'insert#/4,insert#/2,leq#/2,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1 ,true/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/1,c_8/2,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {if'insert#,insert#,leq#,sort#} and constructors {0,cons ,false,nil,s,true} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component sort#(cons(x,xs)) -> c_8(insert#(x,sort(xs)),sort#(xs)) and a lower component if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)) insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys),leq#(x,y)) leq#(s(x),s(y)) -> c_7(leq#(x,y)) Further, following extension rules are added to the lower component. sort#(cons(x,xs)) -> insert#(x,sort(xs)) sort#(cons(x,xs)) -> sort#(xs) ** Step 4.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: sort#(cons(x,xs)) -> c_8(insert#(x,sort(xs)),sort#(xs)) - Weak TRS: if'insert(false(),x,y,ys) -> cons(y,insert(x,ys)) if'insert(true(),x,y,ys) -> cons(x,cons(y,ys)) insert(x,cons(y,ys)) -> if'insert(leq(x,y),x,y,ys) insert(x,nil()) -> cons(x,nil()) leq(0(),y) -> true() leq(s(x),0()) -> false() leq(s(x),s(y)) -> leq(x,y) sort(cons(x,xs)) -> insert(x,sort(xs)) sort(nil()) -> nil() - Signature: {if'insert/4,insert/2,leq/2,sort/1,if'insert#/4,insert#/2,leq#/2,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1 ,true/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/1,c_8/2,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {if'insert#,insert#,leq#,sort#} and constructors {0,cons ,false,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:sort#(cons(x,xs)) -> c_8(insert#(x,sort(xs)),sort#(xs)) -->_2 sort#(cons(x,xs)) -> c_8(insert#(x,sort(xs)),sort#(xs)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: sort#(cons(x,xs)) -> c_8(sort#(xs)) ** Step 4.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: sort#(cons(x,xs)) -> c_8(sort#(xs)) - Weak TRS: if'insert(false(),x,y,ys) -> cons(y,insert(x,ys)) if'insert(true(),x,y,ys) -> cons(x,cons(y,ys)) insert(x,cons(y,ys)) -> if'insert(leq(x,y),x,y,ys) insert(x,nil()) -> cons(x,nil()) leq(0(),y) -> true() leq(s(x),0()) -> false() leq(s(x),s(y)) -> leq(x,y) sort(cons(x,xs)) -> insert(x,sort(xs)) sort(nil()) -> nil() - Signature: {if'insert/4,insert/2,leq/2,sort/1,if'insert#/4,insert#/2,leq#/2,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1 ,true/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {if'insert#,insert#,leq#,sort#} and constructors {0,cons ,false,nil,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: sort#(cons(x,xs)) -> c_8(sort#(xs)) ** Step 4.a:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: sort#(cons(x,xs)) -> c_8(sort#(xs)) - Signature: {if'insert/4,insert/2,leq/2,sort/1,if'insert#/4,insert#/2,leq#/2,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1 ,true/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/1,c_8/1,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {if'insert#,insert#,leq#,sort#} and constructors {0,cons ,false,nil,s,true} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- cons :: ["A"(0) x "A"(1)] -(1)-> "A"(1) sort# :: ["A"(1)] -(15)-> "A"(0) c_8 :: ["A"(0)] -(0)-> "A"(14) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "c_8_A" :: ["A"(0)] -(0)-> "A"(1) "cons_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: sort#(cons(x,xs)) -> c_8(sort#(xs)) 2. Weak: ** Step 4.b:1: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)) insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys),leq#(x,y)) leq#(s(x),s(y)) -> c_7(leq#(x,y)) - Weak DPs: sort#(cons(x,xs)) -> insert#(x,sort(xs)) sort#(cons(x,xs)) -> sort#(xs) - Weak TRS: if'insert(false(),x,y,ys) -> cons(y,insert(x,ys)) if'insert(true(),x,y,ys) -> cons(x,cons(y,ys)) insert(x,cons(y,ys)) -> if'insert(leq(x,y),x,y,ys) insert(x,nil()) -> cons(x,nil()) leq(0(),y) -> true() leq(s(x),0()) -> false() leq(s(x),s(y)) -> leq(x,y) sort(cons(x,xs)) -> insert(x,sort(xs)) sort(nil()) -> nil() - Signature: {if'insert/4,insert/2,leq/2,sort/1,if'insert#/4,insert#/2,leq#/2,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1 ,true/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/1,c_8/2,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {if'insert#,insert#,leq#,sort#} and constructors {0,cons ,false,nil,s,true} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)) insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys),leq#(x,y)) sort#(cons(x,xs)) -> insert#(x,sort(xs)) sort#(cons(x,xs)) -> sort#(xs) and a lower component leq#(s(x),s(y)) -> c_7(leq#(x,y)) Further, following extension rules are added to the lower component. if'insert#(false(),x,y,ys) -> insert#(x,ys) insert#(x,cons(y,ys)) -> if'insert#(leq(x,y),x,y,ys) insert#(x,cons(y,ys)) -> leq#(x,y) sort#(cons(x,xs)) -> insert#(x,sort(xs)) sort#(cons(x,xs)) -> sort#(xs) *** Step 4.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)) insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys),leq#(x,y)) - Weak DPs: sort#(cons(x,xs)) -> insert#(x,sort(xs)) sort#(cons(x,xs)) -> sort#(xs) - Weak TRS: if'insert(false(),x,y,ys) -> cons(y,insert(x,ys)) if'insert(true(),x,y,ys) -> cons(x,cons(y,ys)) insert(x,cons(y,ys)) -> if'insert(leq(x,y),x,y,ys) insert(x,nil()) -> cons(x,nil()) leq(0(),y) -> true() leq(s(x),0()) -> false() leq(s(x),s(y)) -> leq(x,y) sort(cons(x,xs)) -> insert(x,sort(xs)) sort(nil()) -> nil() - Signature: {if'insert/4,insert/2,leq/2,sort/1,if'insert#/4,insert#/2,leq#/2,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1 ,true/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/1,c_8/2,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {if'insert#,insert#,leq#,sort#} and constructors {0,cons ,false,nil,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)) -->_1 insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys),leq#(x,y)):2 2:S:insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys),leq#(x,y)) -->_1 if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)):1 3:W:sort#(cons(x,xs)) -> insert#(x,sort(xs)) -->_1 insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys),leq#(x,y)):2 4:W:sort#(cons(x,xs)) -> sort#(xs) -->_1 sort#(cons(x,xs)) -> sort#(xs):4 -->_1 sort#(cons(x,xs)) -> insert#(x,sort(xs)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys)) *** Step 4.b:1.a:2: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)) insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys)) - Weak DPs: sort#(cons(x,xs)) -> insert#(x,sort(xs)) sort#(cons(x,xs)) -> sort#(xs) - Weak TRS: if'insert(false(),x,y,ys) -> cons(y,insert(x,ys)) if'insert(true(),x,y,ys) -> cons(x,cons(y,ys)) insert(x,cons(y,ys)) -> if'insert(leq(x,y),x,y,ys) insert(x,nil()) -> cons(x,nil()) leq(0(),y) -> true() leq(s(x),0()) -> false() leq(s(x),s(y)) -> leq(x,y) sort(cons(x,xs)) -> insert(x,sort(xs)) sort(nil()) -> nil() - Signature: {if'insert/4,insert/2,leq/2,sort/1,if'insert#/4,insert#/2,leq#/2,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/2,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {if'insert#,insert#,leq#,sort#} and constructors {0,cons ,false,nil,s,true} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> "A"(0) cons :: ["A"(0) x "A"(1)] -(1)-> "A"(1) cons :: ["A"(0) x "A"(6)] -(6)-> "A"(6) cons :: ["A"(0) x "A"(7)] -(7)-> "A"(7) cons :: ["A"(0) x "A"(2)] -(2)-> "A"(2) false :: [] -(0)-> "A"(0) false :: [] -(0)-> "A"(1) false :: [] -(0)-> "A"(15) if'insert :: ["A"(1) x "A"(0) x "A"(0) x "A"(1)] -(3)-> "A"(1) insert :: ["A"(0) x "A"(1)] -(2)-> "A"(1) leq :: ["A"(0) x "A"(0)] -(0)-> "A"(13) nil :: [] -(0)-> "A"(1) nil :: [] -(0)-> "A"(6) nil :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(7) s :: ["A"(0)] -(0)-> "A"(0) sort :: ["A"(6)] -(1)-> "A"(1) true :: [] -(0)-> "A"(1) true :: [] -(0)-> "A"(15) if'insert# :: ["A"(0) x "A"(0) x "A"(0) x "A"(1)] -(0)-> "A"(9) insert# :: ["A"(0) x "A"(1)] -(0)-> "A"(12) sort# :: ["A"(7)] -(15)-> "A"(1) c_1 :: ["A"(0)] -(0)-> "A"(12) c_3 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "0_A" :: [] -(0)-> "A"(1) "c_1_A" :: ["A"(0)] -(0)-> "A"(1) "c_3_A" :: ["A"(0)] -(0)-> "A"(1) "cons_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "false_A" :: [] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "s_A" :: ["A"(0)] -(0)-> "A"(1) "true_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys)) 2. Weak: if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)) *** Step 4.b:1.a:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)) - Weak DPs: insert#(x,cons(y,ys)) -> c_3(if'insert#(leq(x,y),x,y,ys)) sort#(cons(x,xs)) -> insert#(x,sort(xs)) sort#(cons(x,xs)) -> sort#(xs) - Weak TRS: if'insert(false(),x,y,ys) -> cons(y,insert(x,ys)) if'insert(true(),x,y,ys) -> cons(x,cons(y,ys)) insert(x,cons(y,ys)) -> if'insert(leq(x,y),x,y,ys) insert(x,nil()) -> cons(x,nil()) leq(0(),y) -> true() leq(s(x),0()) -> false() leq(s(x),s(y)) -> leq(x,y) sort(cons(x,xs)) -> insert(x,sort(xs)) sort(nil()) -> nil() - Signature: {if'insert/4,insert/2,leq/2,sort/1,if'insert#/4,insert#/2,leq#/2,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1 ,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/0,c_7/1,c_8/2,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {if'insert#,insert#,leq#,sort#} and constructors {0,cons ,false,nil,s,true} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> "A"(0) cons :: ["A"(7) x "A"(7)] -(7)-> "A"(7) cons :: ["A"(14) x "A"(14)] -(14)-> "A"(14) cons :: ["A"(15) x "A"(15)] -(15)-> "A"(15) cons :: ["A"(8) x "A"(8)] -(8)-> "A"(8) false :: [] -(0)-> "A"(1) false :: [] -(0)-> "A"(15) if'insert :: ["A"(1) x "A"(14) x "A"(7) x "A"(7)] -(15)-> "A"(7) insert :: ["A"(14) x "A"(7)] -(8)-> "A"(7) leq :: ["A"(0) x "A"(0)] -(0)-> "A"(15) nil :: [] -(0)-> "A"(7) nil :: [] -(0)-> "A"(14) nil :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(13) s :: ["A"(0)] -(0)-> "A"(0) sort :: ["A"(14)] -(0)-> "A"(7) true :: [] -(0)-> "A"(1) true :: [] -(0)-> "A"(15) if'insert# :: ["A"(1) x "A"(12) x "A"(0) x "A"(7)] -(7)-> "A"(9) insert# :: ["A"(12) x "A"(7)] -(1)-> "A"(12) sort# :: ["A"(15)] -(8)-> "A"(1) c_1 :: ["A"(0)] -(0)-> "A"(11) c_3 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "0_A" :: [] -(0)-> "A"(1) "c_1_A" :: ["A"(0)] -(0)-> "A"(1) "c_3_A" :: ["A"(0)] -(0)-> "A"(1) "cons_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "false_A" :: [] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "s_A" :: ["A"(0)] -(0)-> "A"(1) "true_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: if'insert#(false(),x,y,ys) -> c_1(insert#(x,ys)) 2. Weak: *** Step 4.b:1.b:1: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: leq#(s(x),s(y)) -> c_7(leq#(x,y)) - Weak DPs: if'insert#(false(),x,y,ys) -> insert#(x,ys) insert#(x,cons(y,ys)) -> if'insert#(leq(x,y),x,y,ys) insert#(x,cons(y,ys)) -> leq#(x,y) sort#(cons(x,xs)) -> insert#(x,sort(xs)) sort#(cons(x,xs)) -> sort#(xs) - Weak TRS: if'insert(false(),x,y,ys) -> cons(y,insert(x,ys)) if'insert(true(),x,y,ys) -> cons(x,cons(y,ys)) insert(x,cons(y,ys)) -> if'insert(leq(x,y),x,y,ys) insert(x,nil()) -> cons(x,nil()) leq(0(),y) -> true() leq(s(x),0()) -> false() leq(s(x),s(y)) -> leq(x,y) sort(cons(x,xs)) -> insert(x,sort(xs)) sort(nil()) -> nil() - Signature: {if'insert/4,insert/2,leq/2,sort/1,if'insert#/4,insert#/2,leq#/2,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1 ,true/0,c_1/1,c_2/0,c_3/2,c_4/0,c_5/0,c_6/0,c_7/1,c_8/2,c_9/0} - Obligation: innermost runtime complexity wrt. defined symbols {if'insert#,insert#,leq#,sort#} and constructors {0,cons ,false,nil,s,true} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> "A"(0) cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0) cons :: ["A"(12) x "A"(12)] -(12)-> "A"(12) cons :: ["A"(6) x "A"(6)] -(6)-> "A"(6) false :: [] -(0)-> "A"(0) false :: [] -(0)-> "A"(14) if'insert :: ["A"(0) x "A"(8) x "A"(0) x "A"(0)] -(6)-> "A"(0) insert :: ["A"(8) x "A"(0)] -(6)-> "A"(0) leq :: ["A"(0) x "A"(0)] -(0)-> "A"(6) nil :: [] -(0)-> "A"(0) nil :: [] -(0)-> "A"(12) nil :: [] -(0)-> "A"(14) s :: ["A"(1)] -(1)-> "A"(1) s :: ["A"(0)] -(0)-> "A"(0) sort :: ["A"(12)] -(2)-> "A"(0) true :: [] -(0)-> "A"(0) true :: [] -(0)-> "A"(6) if'insert# :: ["A"(0) x "A"(1) x "A"(0) x "A"(0)] -(6)-> "A"(6) insert# :: ["A"(1) x "A"(0)] -(6)-> "A"(6) leq# :: ["A"(1) x "A"(0)] -(5)-> "A"(8) sort# :: ["A"(12)] -(3)-> "A"(0) c_7 :: ["A"(0)] -(0)-> "A"(14) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "0_A" :: [] -(0)-> "A"(1) "c_7_A" :: ["A"(0)] -(0)-> "A"(1) "cons_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "false_A" :: [] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "s_A" :: ["A"(1)] -(1)-> "A"(1) "true_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: leq#(s(x),s(y)) -> c_7(leq#(x,y)) 2. Weak: WORST_CASE(?,O(n^3))